3.11.1.5 Grammar Rules

3.11.1.5 Grammar Rules

specification

: (specBody)*

;

specBody

: define

| channel

| choreography

| orchstration

| assertion

;

choreography

: 'Chor' ID '{' definition+ '}'

;

orchstration

: 'Orch' ID '{' role+ '}'

;

role : 'Role' ID ('[' INT | '*' ']')? '{' roleBody* '}' //INT means the number of the roles, * mean infinite number of roles

;

roleBody

: letDefintion

| definition

;

letDefintion

: 'var' ID variableRange? ('=' expression)? ';'

| 'var' ID variableRange? '=' recordExpression ';'

| 'var' ID ('[' expression ']')+ variableRange? ('=' recordExpression)? ';' //multi-dimensional array is supported

;

variableRange

: ':' '{' additiveExpression? '..' additiveExpression? '}'

;

recordExpression

: '[' recordElement (',' recordElement)* ']'

;

recordElement

: e1=expression ('(' e2=expression ')')? //e2 means the number of e1, by default it's 1

| e1=expression '..' e2=expression //e1 to e2 gives a range of constants

;

define

: '#' 'define' ID '-'? INT ';'

| '#' 'define' ID ('true' | 'false') ';'

| 'enum' '{' ID (',' ID)* '}' ';'

| '#' 'define' ID conditionalOrExpression ';'

;

channel

: 'channel' ID additiveExpression? ';'

;

assertion

: '#' 'assert' ID

(

( '|=' ( '(' | ')' | '[]' | '<>' | ID | STRING | '!' | '&&' | '||' | '->' | '<->' | '/\\' | '\\/' | '.' | INT )+ )

| 'deadlockfree'

| 'reaches' ID

| 'refines' ID

)

';'

;

statement

: block

| localVariableDeclaration

| ifExpression

| whileExpression

| expression ';'

| ';'

;

//local variable that can be used in the block
localVariableDeclaration
: 'var' ID ('=' expression)? ';'

| 'var' ID '=' recordExpression ';'

;

expression

: conditionalOrExpression ('=' expression)?

;

conditionalOrExpression

: conditionalAndExpression ( '||' conditionalAndExpression )*

;

conditionalAndExpression

: equalityExpression ( '&&' equalityExpression)*

;

equalityExpression

: relationalExpression ( ('=='|'!=') relationalExpression)*

;

relationalExpression

: additiveExpression ( ('<' | '>' | '<=' | '>=') additiveExpression)*

;

additiveExpression

: multiplicativeExpression ( ('+' | '-') multiplicativeExpression)*

;

multiplicativeExpression

: unaryExpression ( ('*' | '/' | '%' ) unaryExpression)*

;

unaryExpression

: '+' unaryExpression

| '-' unaryExpression

| '!' unaryExpressionNotPlusMinus

| unaryExpressionNotPlusMinus

;

unaryExpressionNotPlusMinus

: ID ('[' conditionalOrExpression ']')?

| ID '.' ID

| INT

| 'true'

| 'false'

| '(' conditionalOrExpression ')'

| 'call' '(' ID ',' conditionalOrExpression (',' conditionalOrExpression)? ')'

;

ifExpression

: 'if' '(' expression ')' statement ('else' statement)?

;

whileExpression

: 'while' '(' expression '}' statement

;

recordExpression

: '[' expression (',' expression)* ']'

;

definition

: ID ('(' (ID (',' ID )*)? ')')? '=' interleaveExpr ';'

;

//these rules below give the precedence of the operators, the losest one is interleave.

interleaveExpr

: externalChoiceExpr ('|||' externalChoiceExpr+)*

| '|||' (paralDef (';' paralDef )*) '@' interleaveExpr

;

paralDef

: ID ':' '{' additiveExpression (',' additiveExpression)* '}'

| ID ':' '{' additiveExpression '..' additiveExpression '}'

;

externalChoiceExpr

: sequentialExpr ('[]' sequentialExpr)*

| '[]' (paralDef (';' paralDef )*) '@' interleaveExpr

;

sequentialExpr

: guardExpr (';' guardExpr)*

;

guardExpr

: '[' conditionalOrExpression ']' assignmentExpr

| assignmentExpr

;

assignmentExpr

: block '->' assignmentExpr

| channelCommunicationExpr

;

channelCommunicationExpr

: name=ID '(' caller=ID ',' callee=ID ',' msg=ID ( '.' additiveExpression)* ')' '->' assignmentExpr

| serviceInvocationExpr

;

serviceInvocationExpr

: name=ID '(' caller=ID ',' callee=ID ',' '{' (conditionalOrExpression (',' conditionalOrExpression )*)? '}' ')' '->' assignmentExpr

| channelExpr

;

channelExpr

: name=ID '!' msg=ID ( '.' conditionalOrExpression)* '->' assignmentExpr

| name=ID '?' msg=ID ( '.' conditionalOrExpression)* '->' assignmentExpr

| serviceInvokingExpr

;

serviceInvokingExpr

: ID '!' '{' (ID ('[' INT ']')? (',' ID ('[' INT ']')? )*) '}' '->' assignmentExpr //('[' INT ']')? gives the size of the channel

| ID '?' '{' (ID (',' ID)*) '}' '->' assignmentExpr

| caseExpr

;

caseExpr

: 'case'

(

'{'

caseCondition+

('default' ':' elsec=interleaveExpr)?

'}'

)

| ifExpr

;

caseCondition :

(conditionalOrExpression ':' interleaveExpr)

;

ifExpr

: atom

| 'if' '(' conditionalOrExpression ')' '{' interleaveExpr '}' ('else' '{' interleaveExpr '}' )?

;

atom

: ID ('(' (expression (',' expression )*)? ')')?

| 'Skip' ('('! ')'!)?

| 'Stop' ('('! ')'!)?

| '(' interleaveExpr ')'

;

ID : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')* ;

WS : (' '|'\r'|'\t'|'\u000C'|'\n') ;

INT : ('0'..'9')+ ;

STRING : '"' (~('\\'|'"') )* '"' ;

COMMENT : '/*' ( options {greedy=false;} : . )* '*/' ;

LINE_COMMENT: '//' ~('\n'|'\r')* '\r'? '\n';